\begin{tabbing}
$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$), ${\it es}$:ES, $i$:Id.
\\[0ex]($\forall$$x$:Id. vartype($i$;$x$) $\subseteq\rho$ ${\it ds}$($x$)?Top)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E. loc($e$) $=$ $i$ $\Rightarrow$ valtype($e$) $\subseteq\rho$ Valtype(${\it da}$;kind($e$)))
\\[0ex]$\Rightarrow$ (\=$\forall$$n$:$\mathbb{N}$, $e_{1}$, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ $i$ \}.\+
\\[0ex]ecl{-}es{-}act(${\it es}$;$n$;$x$)($e_{1}$,$e_{2}$) $\Leftrightarrow$ ecl{-}act(${\it ds}$;${\it da}$;$n$;$x$)(es{-}hist\{i:l\}(${\it es}$;$e_{1}$;$e_{2}$)))
\-
\end{tabbing}